COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	(∀e phi |λu.(u*v)*w = u*(v*w)| listinduction nil sortinfo)
C00009 ENDMK
C⊗;
(∀e phi |λu.(u*v)*w = u*(v*w)| listinduction nil sortinfo)
(rw * |*appendfacts*nil| sortinfo)
(trw |∀x u.(u*v)*w = u*(v*w) ⊃ x~((u*v)*w)=x~(u*(v*w))| |der|)
(rw 37 |*38*nil|)
(∀i (v w) )
74. ∀PHI.(∀X.ATOM X∨PHI(CAR X)∧PHI(CDR X)⊃PHI(X))⊃(∀X.PHI(X))
    deps: NIL

NIL 
the symbol SUBST is unknown - declared to have type ?VTYP1
75. ∀X Y Z.SUBST(X,Y,Z)=
            IF ATOM Z THEN IF Z=Y THEN X ELSE Z
             ELSE SUBST(X,Y,CAR Z)~SUBST(X,Y,CDR Z)
    deps: NIL

NIL 
Done.
NIL 
(deletel)
NIL 
76. ∀X Y Z.SUBST(X,Y,Z)=
            IF ATOM Z THEN IF Z=Y THEN X ELSE Z
             ELSE SUBST(X,Y,CAR Z)~SUBST(X,Y,CDR Z)
    deps: NIL

NIL 
)

* .....done.LISPAX read in 
proof? 
* switched to LISPAX
* 74. ∀PHI.(∀X.ATOM X∨PHI(CAR X)∧PHI(CDR X)⊃PHI(X))⊃(∀X.PHI(X))
    deps: NIL

* 
* 76. ∀X Y Z.SUBST(X,Y,Z)=
            IF ATOM Z THEN IF Z=Y THEN X ELSE Z
             ELSE SUBST(X,Y,CAR Z)~SUBST(X,Y,CDR Z)
    deps: NIL

* 77. (∀X1.ATOM X1∨(λZ.SEXP SUBST(X,Y,Z))(CAR X1)∧(λZ.SEXP SUBST(X,Y,Z))(CDR X1)⊃
          SEXP SUBST(X,Y,X1))⊃(∀X2.SEXP SUBST(X,Y,X2))
    deps: NIL

* 
;WIPEOUT UNDEFINED FUNCTION OBJECT 
QUIT
* .....done.
the proofname LISPAX from the proofs read in 
has been renamed to LISPAX1 to avoid clashes.
redefining linename REVERSEAPPEND
is this o.k.?(y or n): eh? try again
(y or n): eh? try again
(y or n): eh? try again
(y or n): eh? try again
(y or n): eh? try again
(y or n): eh? try again
(y or n): eh? try again
(y or n): eh? try again
(y or n): eh? try again
(y or n): eh? try again
(y or n): eh? try again
(y or n): eh? try again
(y or n): eh? try again
(y or n): eh? try again
(y or n): eh? try again
(y or n): eh? try again
(y or n): redefining linename APPENDFACTS
is this o.k.?(y or n): 
n
eh? try again
(y or n): eh? try again
(y or n): eh? try again
(y or n): eh? try again
(y or n): eh? try again
(y or n): eh? try again
(y or n): eh? try again
(y or n): eh? try again
(y or n): eh? try again
(y or n): proof? 
* proof? 
* .....done.LISPAX read in 
proof? 
* switched to LISPAX
* 74. ∀PHI.(∀X.ATOM X∨PHI(CAR X)∧PHI(CDR X)⊃PHI(X))⊃(∀X.PHI(X))
    deps: NIL

* 
* 
* 77. ∀X Y Z.SUBST(X,Y,Z)=
            IF ATOM Z THEN IF Z=Y THEN X ELSE Z
             ELSE SUBST(X,Y,CAR Z)~SUBST(X,Y,CDR Z)
    deps: NIL

* 
* 79. (∀X.ATOM X∨
        (λZ.∀X Y.SEXP SUBST(X,Y,Z))(CAR X)∧(λZ.∀X Y.SEXP SUBST(X,Y,Z))(CDR X)⊃
         (∀X2 Y.SEXP SUBST(X2,Y,X)))⊃(∀X X1 Y.SEXP SUBST(X1,Y,X))
    deps: NIL

* proof? 
* .....done.LISPAX read in 
proof? 
* switched to LISPAX
* 74. ∀PHI.(∀X.ATOM X∨PHI(CAR X)∧PHI(CDR X)⊃PHI(X))⊃(∀X.PHI(X))
    deps: NIL

* 
* 
* 77. ∀X Y Z.SUBST(X,Y,Z)=
            IF ATOM Z THEN IF Z=Y THEN X ELSE Z
             ELSE SUBST(X,Y,CAR Z)~SUBST(X,Y,CDR Z)
    deps: NIL

* 
* 79. (∀X.ATOM X∨
        (λZ.∀X Y.SEXP SUBST(X,Y,Z))(CAR X)∧(λZ.∀X Y.SEXP SUBST(X,Y,Z))(CDR X)⊃
         (∀X18 Y.SEXP SUBST(X18,Y,X)))⊃(∀X X17 Y.SEXP SUBST(X17,Y,X))
    deps: NIL

* proof? 
* .....done.LISPAX read in 
proof? 
* switched to LISPAX
* 74. ∀PHI.(∀X.ATOM X∨(¬ATOM X∧PHI(CAR X))∧PHI(CDR X)⊃PHI(X))⊃(∀X.PHI(X))
    deps: NIL

* 
* 
* 77. ∀X Y Z.SUBST(X,Y,Z)=
            IF ATOM Z THEN IF Z=Y THEN X ELSE Z
             ELSE SUBST(X,Y,CAR Z)~SUBST(X,Y,CDR Z)
    deps: NIL

* 
* 79. (∀X.ATOM X∨
        ¬ATOM X∧(λZ.∀X Y.SEXP SUBST(X,Y,Z))(CAR X)∧
        (λZ.∀X Y.SEXP SUBST(X,Y,Z))(CDR X)⊃(∀X18 Y.SEXP SUBST(X18,Y,X)))⊃
     (∀X X17 Y.SEXP SUBST(X17,Y,X))
    deps: NIL

* 80. ∀U V W.U*(V*W)=(U*V)*W
    deps: NIL

* 
(trw |∀u v w.u*(v*w)=(u*v)*w| |nil*der*nil|)
(wipe-out)
(get-proofs lispax)
(proof lispax)
(axiom |∀phi.(∀x.(atom x ∨ ¬atom x ∧ phi(car x) ∧ phi(cdr x)) ⊃ phi(x))
                         ⊃ ∀x.phi(x)|)
(lname sexpinduction2)
(decl subst |ground⊗ground⊗ground → ground| constant)
(axiom |∀x y z.subst(x,y,z) = if atom z then (if z = y then x else z)
                              else subst(x,y,car z)~subst(x,y,cdr z)|)
(lname definfo)
(∀e phi |λz.∀x y.sexp(subst(x,y,z))| sexpinduction2
|nil**(simpinfo+sortinfo)*nil|
sortinfo)